@ @p
1:=succ(0):nat. {$1=0'$}
2:=succ(1):nat.	{$2=1'$}
3:=succ(2):nat. {$3=2'$}
4:=succ(3):nat. {$4=3'$}
@#
lemma(x:nat):=eq_transitivity(nat,sum(x,1),succ(sum(x,0)),succ(x),sum_ax2(x,0),
  eq_functionality(nat,nat,sum(x,0),x,sum_ax1(x),succ)):is(sum(x,1),succ(x)).
	{$\T x+1=x'$}
@#
2_plus_2:=eq_transitivity(nat,sum(2,2),succ(sum(2,1)),4,sum_ax2(2,1),
  eq_functionality(nat,nat,sum(2,1),3,lemma(2),succ)):is(sum(2,2),4).
	{$\T 2+2=4$}